Search Results

Documents authored by Czajka, Lukasz

Document
DOI: 10.4230/LIPIcs.FSCD.2022.14
Restricting Tree Grammars with Term Rewriting

Authors: Jan Bessai, Lukasz Czajka, Felix Laarmann, and Jakob Rehof

Published in: LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)

Abstract
We investigate the problem of enumerating all terms generated by a tree-grammar which are also in normal form with respect to a set of directed equations (rewriting relation). To this end we show that deciding emptiness and finiteness of the resulting set is EXPTIME-complete. The emptiness result is inspired by a prior result by Comon and Jacquemard on ground reducibility. The finiteness result is based on modification of pumping arguments used by Comon and Jacquemard. We highlight practical applications and limitations. We provide and evaluate a prototype implementation. Limitations are somewhat surprising in that, while deciding emptiness and finiteness is EXPTIME-complete for linear and nonlinear rewrite relations, the linear case is practically feasible while the nonlinear case is infeasible, even for a trivially small example. The algorithms provided for the linear case also improve on prior practical results by Kallat et al.
Cite as

Jan Bessai, Lukasz Czajka, Felix Laarmann, and Jakob Rehof. Restricting Tree Grammars with Term Rewriting. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 14:1-14:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{bessai_et_al:LIPIcs.FSCD.2022.14,
  author =	{Bessai, Jan and Czajka, Lukasz and Laarmann, Felix and Rehof, Jakob},
  title =	{{Restricting Tree Grammars with Term Rewriting}},
  booktitle =	{7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
  pages =	{14:1--14:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-233-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{228},
  editor =	{Felty, Amy P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.14},
  URN =		{urn:nbn:de:0030-drops-162953},
  doi =		{10.4230/LIPIcs.FSCD.2022.14},
  annote =	{Keywords: tree automata, tree grammar, term rewriting, normalization, emptiness, finiteness}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2016.9
A Shallow Embedding of Pure Type Systems into First-Order Logic

Authors: Lukasz Czajka

Published in: LIPIcs, Volume 97, 22nd International Conference on Types for Proofs and Programs (TYPES 2016)

Abstract
We define a shallow embedding of logical proof-irrelevant Pure Type Systems (piPTSs) into minimal first-order logic. In logical piPTSs a distinguished sort *^p of propositions is assumed. Given a context Gamma and a Gamma-proposition tau, i.e., a term tau such that Gamma |- tau : *^p, the embedding translates tau and Gamma into a first-order formula F_Gamma(tau) and a set of first-order axioms Delta_Gamma. The embedding is not complete in general, but it is strong enough to correctly translate most of piPTS propositions (by completeness we mean that if Gamma |- M : tau is derivable in the piPTS then F_Gamma(tau) is provable in minimal first-order logic from the axioms Delta_Gamma). We show the embedding to be sound, i.e., if F_Gamma(tau) is provable in minimal first-order logic from the axioms Delta_Gamma, then Gamma |- M : tau is derivable in the original system for some term M. The interest in the proposed embedding stems from the fact that it forms a basis of the translations used in the recently developed CoqHammer automation tool for dependent type theory.
Cite as

Lukasz Czajka. A Shallow Embedding of Pure Type Systems into First-Order Logic. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 9:1-9:39, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{czajka:LIPIcs.TYPES.2016.9,
  author =	{Czajka, Lukasz},
  title =	{{A Shallow Embedding of Pure Type Systems into First-Order Logic}},
  booktitle =	{22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
  pages =	{9:1--9:39},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-065-1},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{97},
  editor =	{Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.9},
  URN =		{urn:nbn:de:0030-drops-98533},
  doi =		{10.4230/LIPIcs.TYPES.2016.9},
  annote =	{Keywords: pure type systems, first-order logic, hammers, proof automation, dependent type theory}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2018.13
Term Rewriting Characterisation of LOGSPACE for Finite and Infinite Data

Authors: Lukasz Czajka

Published in: LIPIcs, Volume 108, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)

Abstract
We show that LOGSPACE is characterised by finite orthogonal tail-recursive cons-free constructor term rewriting systems, contributing to a line of research initiated by Neil Jones. We describe a LOGSPACE algorithm which computes constructor normal forms. This algorithm is used in the proof of our main result: that simple stream term rewriting systems characterise LOGSPACE-computable stream functions as defined by Ramyaa and Leivant. This result concerns characterising logarithmic-space computation on infinite streams by means of infinitary rewriting.
Cite as

Lukasz Czajka. Term Rewriting Characterisation of LOGSPACE for Finite and Infinite Data. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 13:1-13:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{czajka:LIPIcs.FSCD.2018.13,
  author =	{Czajka, Lukasz},
  title =	{{Term Rewriting Characterisation of LOGSPACE for Finite and Infinite Data}},
  booktitle =	{3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)},
  pages =	{13:1--13:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-077-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{108},
  editor =	{Kirchner, H\'{e}l\`{e}ne},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.13},
  URN =		{urn:nbn:de:0030-drops-91831},
  doi =		{10.4230/LIPIcs.FSCD.2018.13},
  annote =	{Keywords: LOGSPACE, implicit complexity, term rewriting, infinitary rewriting, streams}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2017.14
Confluence of an Extension of Combinatory Logic by Boolean Constants

Authors: Lukasz Czajka

Published in: LIPIcs, Volume 84, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)

Abstract
We show confluence of a conditional term rewriting system CL-pc^1, which is an extension of Combinatory Logic by Boolean constants. This solves problem 15 from the RTA list of open problems. The proof has been fully formalized in the Coq proof assistant.
Cite as

Lukasz Czajka. Confluence of an Extension of Combinatory Logic by Boolean Constants. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 14:1-14:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{czajka:LIPIcs.FSCD.2017.14,
  author =	{Czajka, Lukasz},
  title =	{{Confluence of an Extension of Combinatory Logic by Boolean Constants}},
  booktitle =	{2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)},
  pages =	{14:1--14:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-047-7},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{84},
  editor =	{Miller, Dale},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.14},
  URN =		{urn:nbn:de:0030-drops-77368},
  doi =		{10.4230/LIPIcs.FSCD.2017.14},
  annote =	{Keywords: combinatory logic, conditional linearization, unique normal form property, confluence}
}
Document
DOI: 10.4230/LIPIcs.RTA.2015.106
Confluence of nearly orthogonal infinitary term rewriting systems

Authors: Lukasz Czajka

Published in: LIPIcs, Volume 36, 26th International Conference on Rewriting Techniques and Applications (RTA 2015)

Abstract
We give a relatively simple coinductive proof of confluence, modulo equivalence of root-active terms, of nearly orthogonal infinitary term rewriting systems. Nearly orthogonal systems allow certain root overlaps, but no non-root overlaps. Using a slightly more complicated method we also show confluence modulo equivalence of hypercollapsing terms. The condition we impose on root overlaps is similar to the condition used by Toyama in the context of finitary rewriting.
Cite as

Lukasz Czajka. Confluence of nearly orthogonal infinitary term rewriting systems. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 106-126, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{czajka:LIPIcs.RTA.2015.106,
  author =	{Czajka, Lukasz},
  title =	{{Confluence of nearly orthogonal infinitary term rewriting  systems}},
  booktitle =	{26th International Conference on Rewriting Techniques and Applications (RTA 2015)},
  pages =	{106--126},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-85-9},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{36},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015.106},
  URN =		{urn:nbn:de:0030-drops-51929},
  doi =		{10.4230/LIPIcs.RTA.2015.106},
  annote =	{Keywords: infinitary rewriting, confluence, coinduction}
}
Document
DOI: 10.4230/LIPIcs.CSL.2011.174
A Semantic Approach to Illative Combinatory Logic

Authors: Lukasz Czajka

Published in: LIPIcs, Volume 12, Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL (2011)

Abstract
This work introduces the theory of illative combinatory algebras, which is closely related to systems of illative combinatory logic. We thus provide a semantic interpretation for a formal framework in which both logic and computation may be expressed in a unified manner. Systems of illative combinatory logic consist of combinatory logic extended with constants and rules of inference intended to capture logical notions. Our theory does not correspond strictly to any traditional system, but draws inspiration from many. It differs from them in that it couples the notion of truth with the notion of equality between terms, which enables the use of logical formulas in conditional expressions. We give a consistency proof for first-order illative combinatory algebras. A complete embedding of classical predicate logic into our theory is also provided. The translation is very direct and natural.
Cite as

Lukasz Czajka. A Semantic Approach to Illative Combinatory Logic. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 174-188, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{czajka:LIPIcs.CSL.2011.174,
  author =	{Czajka, Lukasz},
  title =	{{A Semantic Approach to Illative Combinatory Logic}},
  booktitle =	{Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
  pages =	{174--188},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-32-3},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{12},
  editor =	{Bezem, Marc},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.174},
  URN =		{urn:nbn:de:0030-drops-32303},
  doi =		{10.4230/LIPIcs.CSL.2011.174},
  annote =	{Keywords: illative combinatory logic, term rewriting, first-order logic}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact